update-spec(ds;da)
== kz:KndId fp ((State(ds)Valtype(da;1of(kz))ds(2of(kz))?Void)) List 

latex

---

clarification:

update-spec(ds;da)
== kz:KndId fp ((State(ds)Valtype(da;1of(kz))fpf-cap(ds;IdDeq;2of(kz);Void))) List 

latex

Definitions	a:A fp B(a), Knd, Id, type List, x:AB(x), , State(ds), x:AB(x), Valtype(da;k), 1of(t), f(x)?z, IdDeq, 2of(t), Void
FDL editor aliases	update-spec